\begin{tabbing}
es{-}only{-}sender(${\it es}$; $k$; $B$; $l$; ${\it tg}$; $T$; $s$,$v$.$f$($s$;$v$))
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(\=$\forall$$e$:es{-}E(${\it es}$).\+\+
\\[0ex]es{-}loc(${\it es}$; $e$) $=$ source($l$) $\in$ Id
\\[0ex]$\Rightarrow$ es{-}kind(${\it es}$; $e$) $=$ $k$ $\in$ Knd
\\[0ex]$\Rightarrow$ (\=$\exists$${\it e'}$:es{-}E(${\it es}$).\+
\\[0ex]es{-}kind(${\it es}$; ${\it e'}$) $=$ rcv($l$,${\it tg}$) $\in$ Knd \& es{-}sender(${\it es}$; ${\it e'}$) $=$ $e$ $\in$ es{-}E(${\it es}$)))
\-\-\\[0ex]\& (\=$\forall$${\it e'}$:es{-}E(${\it es}$).\+
\\[0ex]es{-}kind(${\it es}$; ${\it e'}$) $=$ rcv($l$,${\it tg}$) $\in$ Knd
\\[0ex]$\Rightarrow$ \=es{-}kind(${\it es}$; es{-}sender(${\it es}$; ${\it e'}$)) $=$ $k$ $\in$ Knd\+
\\[0ex]\& es{-}valtype(${\it es}$; es{-}sender(${\it es}$; ${\it e'}$)) $\subseteq\rho$ $B$
\\[0ex]\& es{-}valtype(${\it es}$; ${\it e'}$) $\subseteq\rho$ $T$
\\[0ex]\& \=es{-}val(${\it es}$; ${\it e'}$)\+
\\[0ex]$=$
\\[0ex]$f$(es{-}state{-}when(${\it es}$;es{-}sender(${\it es}$; ${\it e'}$));es{-}val(${\it es}$; es{-}sender(${\it es}$; ${\it e'}$)))
\\[0ex]$\in$ $T$
\\[0ex]\& (\=$\forall$${\it e''}$:es{-}E(${\it es}$).\+
\\[0ex]es{-}kind(${\it es}$; ${\it e''}$) $=$ rcv($l$,${\it tg}$) $\in$ Knd
\\[0ex]$\Rightarrow$ es{-}sender(${\it es}$; ${\it e''}$) $=$ es{-}sender(${\it es}$; ${\it e'}$) $\in$ es{-}E(${\it es}$)
\\[0ex]$\Rightarrow$ ${\it e''}$ $=$ ${\it e'}$ $\in$ es{-}E(${\it es}$)))
\-\-\-\-\-
\end{tabbing}